Date: Wed, 20 Nov 1996 23:00:46 GMT
Server: NCSA/1.5
Content-type: text/html
Last-modified: Wed, 23 Mar 1994 00:46:34 GMT
Content-length: 2490

<HTML>
<HEAD>
<title>Harry R. Lewis</title>
</HEAD>
<BODY>
<h1>Harry Lewis</h1>
<!WA0><img align=top src=http://www.das.harvard.edu/users/faculty/Harry_Lewis/Harry_Lewis.gif>
<h3>Gordon McKay Professor of Computer Science</h3>
<h3>THEORY OF COMPUTATION AND COMPUTER SYSTEMS </h3>
Theoretical computer science has its roots in mathematical
logic. In the 1930s, using mathematical automata, Turing 
investigated whether the truth of mathematical propositions
could be determined by algorithmic procedures; since then,
studies of formalized computers and formalized mathematical
systems have continued to complement and enrich one another. 
<p>
Professor Lewis has worked extensively on the algorithmic
solvability of logical, computational, and combinatorial
systems, attempting to clarify the relations between them
and to identify their common characteristics. For example,
he has applied automata theory to the classical predicate 
calculus and to circuit models for parallel computers.
<p>
Currently he is working on practical formal methods for 
design verification of asynchronous systems, such as
boolean circuits and signalling protocols.  Timing characteristics
of such systems are notoriously difficult to validate under
realistic models of their behavior, and
most practical computer-aided design tools rely on inexhaustive
simulation rather than complete verification. Professor Lewis
has developed both a theoretical logical framework for 
the timing specification of asynchronous systems, and 
software that uses this specification language
to verify the functionality of asynchronous boolean circuits
whose components have specified minimum and maximum time delays.
<p>
Professor Lewis is actively involved in the use of computers in education,
and his books have had a significant influence on
the teaching of the foundations of computer science to undergraduates.
<hr>
<ul>
<li>H. R. Lewis and L. Deneberg, <i>Data Structures and Their
Algorithms</i>, HarperCollins Publishers, New York, NY (1991). 

<li><i>A logic of concrete time intervals,</i> Proc. Fifth Annual IEEE
Symposium on Logic in Computer Science, IEEE, 380-389 (1990).

<li>H. R. Lewis and J. Tecosky, <i>MacFunction (Software for the Apple
MacIntosh),</i> True Basic, Inc., Hanover, NH, (1987).

<li>H. R. Lewis and C. H. Papadimitriou, <i>Elements of the Theory of
Computation</i>, Prentice-Hall, Englewood Cliffs, N. J. (1981).

<li><i>Complexity results for classes of quantificational formulas,</i>
J.Comput. Syst. Sci. \fB21,\fR 317 (1980).
</ul>
</BODY>
</HTML>
